(set-logic QF_NIA)
(set-info :source |verymax-execution|)
(set-info :smt-lib-version 2.0)
(declare-fun Nl10__const_65536^01 () Int)
(declare-fun Nl10fcode5^01 () Int)
(declare-fun Nl10hshift11^01 () Int)
(declare-fun lam0n0 () Int)
(declare-fun lam0n1 () Int)
(declare-fun lam0n2 () Int)
(declare-fun Nl10CT1 () Int)
(declare-fun lam1n0 () Int)
(declare-fun lam1n1 () Int)
(declare-fun lam1n2 () Int)
(declare-fun lam2n0 () Int)
(declare-fun lam2n1 () Int)
(declare-fun lam2n2 () Int)
(declare-fun lam2n3 () Int)
(declare-fun lam2n4 () Int)
(declare-fun lam3n0 () Int)
(declare-fun lam3n1 () Int)
(declare-fun lam3n2 () Int)
(declare-fun lam3n3 () Int)
(declare-fun lam3n4 () Int)
(declare-fun lam3n5 () Int)
(declare-fun lam4n0 () Int)
(declare-fun lam4n1 () Int)
(declare-fun lam4n2 () Int)
(declare-fun lam4n3 () Int)
(declare-fun lam4n4 () Int)
(declare-fun lam4n5 () Int)
(declare-fun lam5n0 () Int)
(declare-fun lam5n1 () Int)
(declare-fun lam5n2 () Int)
(declare-fun lam5n3 () Int)
(declare-fun lam5n4 () Int)
(declare-fun lam6n0 () Int)
(declare-fun lam6n1 () Int)
(declare-fun lam6n2 () Int)
(declare-fun lam6n3 () Int)
(declare-fun lam6n4 () Int)
(declare-fun lam6n5 () Int)
(declare-fun lam7n0 () Int)
(declare-fun lam7n1 () Int)
(declare-fun lam7n2 () Int)
(declare-fun lam7n3 () Int)
(declare-fun lam7n4 () Int)
(declare-fun lam7n5 () Int)
(declare-fun lam8n0 () Int)
(declare-fun lam8n1 () Int)
(declare-fun lam8n2 () Int)
(declare-fun lam8n3 () Int)
(declare-fun lam8n4 () Int)
(declare-fun lam9n0 () Int)
(declare-fun lam9n1 () Int)
(declare-fun lam9n2 () Int)
(declare-fun lam9n3 () Int)
(declare-fun lam9n4 () Int)
(declare-fun lam9n5 () Int)
(declare-fun lam10n0 () Int)
(declare-fun lam10n1 () Int)
(declare-fun lam10n2 () Int)
(declare-fun lam10n3 () Int)
(declare-fun lam10n4 () Int)
(declare-fun lam10n5 () Int)
(declare-fun pBounded () Bool)
(declare-fun RFN1___const_65536^0 () Int)
(declare-fun RFN1_fcode5^0 () Int)
(declare-fun RFN1_hshift11^0 () Int)
(declare-fun lam14n0 () Int)
(declare-fun lam14n1 () Int)
(declare-fun lam14n2 () Int)
(declare-fun lam14n3 () Int)
(declare-fun lam14n4 () Int)
(declare-fun RFN1_CT () Int)
(declare-fun lam13n0 () Int)
(declare-fun lam13n1 () Int)
(declare-fun lam13n2 () Int)
(declare-fun lam13n3 () Int)
(declare-fun lam13n4 () Int)
(declare-fun lam12n0 () Int)
(declare-fun lam12n1 () Int)
(declare-fun lam12n2 () Int)
(declare-fun lam12n3 () Int)
(declare-fun lam12n4 () Int)
(declare-fun lam11n0 () Int)
(declare-fun lam11n1 () Int)
(declare-fun lam11n2 () Int)
(declare-fun lam11n3 () Int)
(declare-fun lam11n4 () Int)
(assert ( and ( <= ( - 1 ) Nl10__const_65536^01 ) ( <= Nl10__const_65536^01 1 ) ( <= ( - 1 ) Nl10fcode5^01 ) ( <= Nl10fcode5^01 1 ) ( <= ( - 1 ) Nl10hshift11^01 ) ( <= Nl10hshift11^01 1 ) ))
(assert ( or ( and ( >= lam0n0 0 ) ( >= lam0n1 0 ) ( >= lam0n2 0 ) ( > ( + ( * 1 lam0n0 ) ( * ( - 1 ) lam0n1 ) ( * Nl10CT1 lam0n2 ) ( - 1 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * Nl10__const_65536^01 lam0n2 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * Nl10fcode5^01 lam0n2 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n1 ) ( * Nl10hshift11^01 lam0n2 ) ) 0 ) ) ( and ( >= lam1n0 0 ) ( >= lam1n1 0 ) ( >= lam1n2 0 ) ( > ( + ( * 1 lam1n0 ) ( * ( - 1 ) lam1n1 ) ( * Nl10CT1 lam1n2 ) ( - 1 ( + ( + Nl10CT1 ( * Nl10fcode5^01 0 ) ) ( * Nl10hshift11^01 1 ) ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam1n0 ) ( * Nl10__const_65536^01 lam1n2 ) ( - ( + 0 Nl10__const_65536^01 ) ) ) 0 ) ( = ( + ( * 1 lam1n0 ) ( * Nl10fcode5^01 lam1n2 ) ) 0 ) ( = ( + ( * ( - 1 ) lam1n1 ) ( * Nl10hshift11^01 lam1n2 ) ( - ( + 0 ( * Nl10hshift11^01 1 ) ) ) ) 0 ) ( = ( - ( + 0 ( * Nl10fcode5^01 1 ) ) ) 0 ) ) ))
(assert ( and ( and ( >= lam2n0 0 ) ( >= lam2n1 0 ) ( >= lam2n2 0 ) ( > ( + ( * 1 lam2n2 ) ( - 1 ( + ( + Nl10CT1 ( * Nl10fcode5^01 0 ) ) ( * Nl10hshift11^01 0 ) ) ) ) 0 ) ( = ( * 1 lam2n3 ) 0 ) ( = ( + ( * ( - 1 ) lam2n2 ) ( - ( + 0 Nl10__const_65536^01 ) ) ) 0 ) ( = ( * 1 lam2n4 ) 0 ) ( = ( + ( * 1 lam2n0 ) ( * 1 lam2n1 ) ) 0 ) ( = ( + ( * 1 lam2n2 ) ( - ( + 0 ( * Nl10fcode5^01 1 ) ) ) ) 0 ) ( = ( * ( - 1 ) lam2n1 ) 0 ) ( = ( * ( - 1 ) lam2n3 ) 0 ) ) ( and ( >= lam3n0 0 ) ( >= lam3n1 0 ) ( >= lam3n2 0 ) ( >= lam3n3 0 ) ( > ( + ( * 1 lam3n2 ) ( * 1 lam3n3 ) ( - 1 ( + ( + Nl10CT1 ( * Nl10fcode5^01 0 ) ) ( * Nl10hshift11^01 0 ) ) ) ) 0 ) ( = ( * 1 lam3n4 ) 0 ) ( = ( * 1 lam3n0 ) 0 ) ( = ( + ( * ( - 1 ) lam3n2 ) ( - ( + 0 Nl10__const_65536^01 ) ) ) 0 ) ( = ( * 1 lam3n5 ) 0 ) ( = ( + ( * 1 lam3n1 ) ( * ( - 1 ) lam3n3 ) ) 0 ) ( = ( + ( * 1 lam3n2 ) ( - ( + 0 ( * Nl10fcode5^01 1 ) ) ) ) 0 ) ( = ( * ( - 1 ) lam3n1 ) 0 ) ( = ( * ( - 1 ) lam3n4 ) 0 ) ) ( and ( >= lam4n0 0 ) ( >= lam4n1 0 ) ( >= lam4n2 0 ) ( >= lam4n3 0 ) ( > ( + ( * 1 lam4n1 ) ( * 1 lam4n2 ) ( * 1 lam4n3 ) ( - 1 ( + ( + Nl10CT1 ( * Nl10fcode5^01 0 ) ) ( * Nl10hshift11^01 0 ) ) ) ) 0 ) ( = ( * ( - 1 ) lam4n1 ) 0 ) ( = ( + ( * ( - 1 ) lam4n2 ) ( - ( + 0 Nl10__const_65536^01 ) ) ) 0 ) ( = ( * 1 lam4n4 ) 0 ) ( = ( + ( * 1 lam4n0 ) ( * ( - 1 ) lam4n3 ) ) 0 ) ( = ( + ( * 1 lam4n2 ) ( - ( + 0 ( * Nl10fcode5^01 1 ) ) ) ) 0 ) ( = ( * ( - 1 ) lam4n0 ) 0 ) ( = ( * 1 lam4n5 ) 0 ) ( = ( * ( - 1 ) lam4n5 ) 0 ) ) ( and ( >= lam5n0 0 ) ( >= lam5n1 0 ) ( >= lam5n2 0 ) ( >= lam5n3 0 ) ( > ( + ( * 1 lam5n2 ) ( * 1 lam5n3 ) ( - 1 ( + ( + Nl10CT1 ( * Nl10fcode5^01 0 ) ) ( * Nl10hshift11^01 0 ) ) ) ) 0 ) ( = ( * 1 lam5n4 ) 0 ) ( = ( + ( * ( - 1 ) lam5n2 ) ( - ( + 0 Nl10__const_65536^01 ) ) ) 0 ) ( = ( * ( - 1 ) lam5n3 ) 0 ) ( = ( + ( * 1 lam5n0 ) ( * 1 lam5n1 ) ) 0 ) ( = ( + ( * 1 lam5n2 ) ( - ( + 0 ( * Nl10fcode5^01 1 ) ) ) ) 0 ) ( = ( * ( - 1 ) lam5n1 ) 0 ) ( = ( * ( - 1 ) lam5n4 ) 0 ) ) ( and ( >= lam6n0 0 ) ( >= lam6n1 0 ) ( >= lam6n2 0 ) ( >= lam6n3 0 ) ( >= lam6n4 0 ) ( > ( + ( * 1 lam6n2 ) ( * 1 lam6n3 ) ( * 1 lam6n4 ) ( - 1 ( + ( + Nl10CT1 ( * Nl10fcode5^01 0 ) ) ( * Nl10hshift11^01 0 ) ) ) ) 0 ) ( = ( * 1 lam6n5 ) 0 ) ( = ( * 1 lam6n0 ) 0 ) ( = ( + ( * ( - 1 ) lam6n2 ) ( - ( + 0 Nl10__const_65536^01 ) ) ) 0 ) ( = ( * ( - 1 ) lam6n3 ) 0 ) ( = ( + ( * 1 lam6n1 ) ( * ( - 1 ) lam6n4 ) ) 0 ) ( = ( + ( * 1 lam6n2 ) ( - ( + 0 ( * Nl10fcode5^01 1 ) ) ) ) 0 ) ( = ( * ( - 1 ) lam6n1 ) 0 ) ( = ( * ( - 1 ) lam6n5 ) 0 ) ) ( and ( >= lam7n0 0 ) ( >= lam7n1 0 ) ( >= lam7n2 0 ) ( >= lam7n3 0 ) ( >= lam7n4 0 ) ( > ( + ( * 1 lam7n1 ) ( * 1 lam7n2 ) ( * 1 lam7n3 ) ( * 1 lam7n4 ) ( - 1 ( + ( + Nl10CT1 ( * Nl10fcode5^01 0 ) ) ( * Nl10hshift11^01 0 ) ) ) ) 0 ) ( = ( * ( - 1 ) lam7n1 ) 0 ) ( = ( + ( * ( - 1 ) lam7n2 ) ( - ( + 0 Nl10__const_65536^01 ) ) ) 0 ) ( = ( * ( - 1 ) lam7n3 ) 0 ) ( = ( + ( * 1 lam7n0 ) ( * ( - 1 ) lam7n4 ) ) 0 ) ( = ( + ( * 1 lam7n2 ) ( - ( + 0 ( * Nl10fcode5^01 1 ) ) ) ) 0 ) ( = ( * ( - 1 ) lam7n0 ) 0 ) ( = ( * 1 lam7n5 ) 0 ) ( = ( * ( - 1 ) lam7n5 ) 0 ) ) ( and ( >= lam8n0 0 ) ( >= lam8n1 0 ) ( >= lam8n2 0 ) ( >= lam8n3 0 ) ( > ( + ( * 1 lam8n2 ) ( * 1 lam8n3 ) ( - 1 ( + ( + Nl10CT1 ( * Nl10fcode5^01 0 ) ) ( * Nl10hshift11^01 0 ) ) ) ) 0 ) ( = ( * 1 lam8n4 ) 0 ) ( = ( + ( * ( - 1 ) lam8n2 ) ( - ( + 0 Nl10__const_65536^01 ) ) ) 0 ) ( = ( * 1 lam8n3 ) 0 ) ( = ( + ( * 1 lam8n0 ) ( * 1 lam8n1 ) ) 0 ) ( = ( + ( * 1 lam8n2 ) ( - ( + 0 ( * Nl10fcode5^01 1 ) ) ) ) 0 ) ( = ( * ( - 1 ) lam8n1 ) 0 ) ( = ( * ( - 1 ) lam8n4 ) 0 ) ) ( and ( >= lam9n0 0 ) ( >= lam9n1 0 ) ( >= lam9n2 0 ) ( >= lam9n3 0 ) ( >= lam9n4 0 ) ( > ( + ( * 1 lam9n2 ) ( * 1 lam9n3 ) ( * 1 lam9n4 ) ( - 1 ( + ( + Nl10CT1 ( * Nl10fcode5^01 0 ) ) ( * Nl10hshift11^01 0 ) ) ) ) 0 ) ( = ( * 1 lam9n5 ) 0 ) ( = ( * 1 lam9n0 ) 0 ) ( = ( + ( * ( - 1 ) lam9n2 ) ( - ( + 0 Nl10__const_65536^01 ) ) ) 0 ) ( = ( * 1 lam9n3 ) 0 ) ( = ( + ( * 1 lam9n1 ) ( * ( - 1 ) lam9n4 ) ) 0 ) ( = ( + ( * 1 lam9n2 ) ( - ( + 0 ( * Nl10fcode5^01 1 ) ) ) ) 0 ) ( = ( * ( - 1 ) lam9n1 ) 0 ) ( = ( * ( - 1 ) lam9n5 ) 0 ) ) ( and ( >= lam10n0 0 ) ( >= lam10n1 0 ) ( >= lam10n2 0 ) ( >= lam10n3 0 ) ( >= lam10n4 0 ) ( > ( + ( * 1 lam10n1 ) ( * 1 lam10n2 ) ( * 1 lam10n3 ) ( * 1 lam10n4 ) ( - 1 ( + ( + Nl10CT1 ( * Nl10fcode5^01 0 ) ) ( * Nl10hshift11^01 0 ) ) ) ) 0 ) ( = ( * ( - 1 ) lam10n1 ) 0 ) ( = ( + ( * ( - 1 ) lam10n2 ) ( - ( + 0 Nl10__const_65536^01 ) ) ) 0 ) ( = ( * 1 lam10n3 ) 0 ) ( = ( + ( * 1 lam10n0 ) ( * ( - 1 ) lam10n4 ) ) 0 ) ( = ( + ( * 1 lam10n2 ) ( - ( + 0 ( * Nl10fcode5^01 1 ) ) ) ) 0 ) ( = ( * ( - 1 ) lam10n0 ) 0 ) ( = ( * 1 lam10n5 ) 0 ) ( = ( * ( - 1 ) lam10n5 ) 0 ) ) ))
(assert ( or ( not pBounded ) ( and ( or ( not ( = RFN1___const_65536^0 0 ) ) ( not ( = RFN1_fcode5^0 0 ) ) ( >= RFN1_hshift11^0 0 ) ) ( or ( <= RFN1___const_65536^0 0 ) ( not ( = RFN1_fcode5^0 0 ) ) ( >= RFN1_hshift11^0 0 ) ) ( or ( >= RFN1___const_65536^0 0 ) ( not ( = RFN1_fcode5^0 0 ) ) ( >= RFN1_hshift11^0 0 ) ) ) ))
(assert ( or ( and ( and ( >= lam14n0 0 ) ( >= lam14n1 0 ) ( >= lam14n2 0 ) ( >= lam14n3 0 ) ( >= lam14n4 0 ) ( > ( + ( * 1 lam14n0 ) ( * 50001 lam14n1 ) ( * 50001 lam14n2 ) ( * 50001 lam14n3 ) ( * Nl10CT1 lam14n4 ) ( - 1 ( - ( + ( + RFN1_CT ( * RFN1_fcode5^0 0 ) ) ( * RFN1_hshift11^0 1 ) ) RFN1_CT ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam14n0 ) ( * 1 lam14n1 ) ( * ( - 1 ) lam14n2 ) ( * Nl10__const_65536^01 lam14n4 ) ( - ( - ( + 0 RFN1___const_65536^0 ) RFN1___const_65536^0 ) ) ) 0 ) ( = ( + ( * 1 lam14n0 ) ( * Nl10fcode5^01 lam14n4 ) ( - ( - RFN1_fcode5^0 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam14n1 ) ( * ( - 1 ) lam14n2 ) ( * ( - 1 ) lam14n3 ) ( * Nl10hshift11^01 lam14n4 ) ( - ( - ( + 0 ( * RFN1_hshift11^0 1 ) ) RFN1_hshift11^0 ) ) ) 0 ) ( = ( - ( + 0 ( * RFN1_fcode5^0 1 ) ) ) 0 ) ) ( and ( and ( >= lam13n0 0 ) ( >= lam13n1 0 ) ( >= lam13n2 0 ) ( >= lam13n3 0 ) ( >= lam13n4 0 ) ( > ( + ( * 1 lam13n0 ) ( * 50001 lam13n1 ) ( * 50001 lam13n2 ) ( * 50001 lam13n3 ) ( * Nl10CT1 lam13n4 ) ( - 1 ( + ( - ( + ( + RFN1_CT ( * RFN1_fcode5^0 0 ) ) ( * RFN1_hshift11^0 1 ) ) RFN1_CT ) 1 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam13n0 ) ( * 1 lam13n1 ) ( * ( - 1 ) lam13n2 ) ( * Nl10__const_65536^01 lam13n4 ) ( - ( - ( + 0 RFN1___const_65536^0 ) RFN1___const_65536^0 ) ) ) 0 ) ( = ( + ( * 1 lam13n0 ) ( * Nl10fcode5^01 lam13n4 ) ( - ( - RFN1_fcode5^0 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam13n1 ) ( * ( - 1 ) lam13n2 ) ( * ( - 1 ) lam13n3 ) ( * Nl10hshift11^01 lam13n4 ) ( - ( - ( + 0 ( * RFN1_hshift11^0 1 ) ) RFN1_hshift11^0 ) ) ) 0 ) ( = ( - ( + 0 ( * RFN1_fcode5^0 1 ) ) ) 0 ) ) ( or ( and ( >= lam12n0 0 ) ( >= lam12n1 0 ) ( >= lam12n2 0 ) ( >= lam12n3 0 ) ( >= lam12n4 0 ) ( > ( + ( * 1 lam12n0 ) ( * 50001 lam12n1 ) ( * 50001 lam12n2 ) ( * 50001 lam12n3 ) ( * Nl10CT1 lam12n4 ) ( - 1 ( - RFN1_CT ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam12n0 ) ( * 1 lam12n1 ) ( * ( - 1 ) lam12n2 ) ( * Nl10__const_65536^01 lam12n4 ) ( - ( - RFN1___const_65536^0 ) ) ) 0 ) ( = ( + ( * 1 lam12n0 ) ( * Nl10fcode5^01 lam12n4 ) ( - ( - RFN1_fcode5^0 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam12n1 ) ( * ( - 1 ) lam12n2 ) ( * ( - 1 ) lam12n3 ) ( * Nl10hshift11^01 lam12n4 ) ( - ( - RFN1_hshift11^0 ) ) ) 0 ) ) pBounded ) ) ) ( and ( >= lam11n0 0 ) ( >= lam11n1 0 ) ( >= lam11n2 0 ) ( >= lam11n3 0 ) ( >= lam11n4 0 ) ( > ( + ( * 1 lam11n0 ) ( * 50001 lam11n1 ) ( * 50001 lam11n2 ) ( * 50001 lam11n3 ) ( * Nl10CT1 lam11n4 ) ( - 1 ) ) 0 ) ( = ( + ( * ( - 1 ) lam11n0 ) ( * 1 lam11n1 ) ( * ( - 1 ) lam11n2 ) ( * Nl10__const_65536^01 lam11n4 ) ) 0 ) ( = ( + ( * 1 lam11n0 ) ( * Nl10fcode5^01 lam11n4 ) ) 0 ) ( = ( + ( * ( - 1 ) lam11n1 ) ( * ( - 1 ) lam11n2 ) ( * ( - 1 ) lam11n3 ) ( * Nl10hshift11^01 lam11n4 ) ) 0 ) ) ))
(check-sat)
(exit)



